// buffer_read_double()
// Reads a double from the buffer.

return buffer_read(buffer, buffer_f64)
